T:Type, as,as',bs,cs:(T List).
(||as|| = ||as'||  )  (append(cs; as) = append(bs; as')  (T List))  (cs = bs) 

latex

Definitions	append(as; bs), prop{i:l}, P  Q, guard(T), P  Q, ||as||, x:A. B(x), t  T, P  Q
Lemmas	length wf1, general-append-cancellation, append wf